package com.googlecode.kipler.satisfiability.completion.rule.individual;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.ConceptCategory;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.satisfiability.blocking.abox.ABoxBlockingStrategy;
import com.googlecode.kipler.satisfiability.completion.branching.ChooseRuleBranchingPoint;
import com.googlecode.kipler.satisfiability.reasoner.BranchingException;
import com.googlecode.kipler.satisfiability.reasoner.Reasoner;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.QualifiedNoRestriction;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.ObjectRoleAssertion;
import com.googlecode.kipler.transformations.ConceptSimplificationVisitor;


/**
 * 
 * @author İnanç Seylan
 *
 */
public class ChooseRule extends ABoxRule {
	private ABox aBox;

	private boolean applied;

	private Reasoner prover;

	private ConceptAssertion reasonForApplication;

	private ABoxBlockingStrategy blocking;

	public ChooseRule(Reasoner prover, ABoxBlockingStrategy blocking) {
		this.prover = prover;
		setBlocking(blocking);
	}

	public ABoxBlockingStrategy getBlocking() {
		return blocking;
	}

	public void setBlocking(ABoxBlockingStrategy blocking) {
		this.blocking = blocking;
	}

	@Override
	public boolean isApplied() {
		return applied;
	}

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		aBox = getWorld().getABox();
		if (!getBlocking().isIndirectlyBlocked(aBox, getIndividual().getName())) {
			for (Iterator<Concept> i = getIndividual().conceptIterator(
					ConceptCategory.AT_LEAST); i.hasNext();) {
				Concept concept = i.next();
				reasonForApplication = new ConceptAssertion(concept,
						getIndividual().getName());
				addConceptToNeighbors((QualifiedNoRestriction) concept);
			}
			for (Iterator<Concept> i = getIndividual().conceptIterator(
					ConceptCategory.AT_MOST); i.hasNext();) {
				Concept concept = i.next();
				reasonForApplication = new ConceptAssertion(concept,
						getIndividual().getName());
				addConceptToNeighbors((QualifiedNoRestriction) concept);
			}
		}
	}

	/**
	 * @param qr
	 * @throws BranchingException
	 */
	private void addConceptToNeighbors(QualifiedNoRestriction qr)
			throws ReasonerException {
		Iterator<ObjectRoleAssertion> raIter = aBox.neighborIterator(qr
				.getRole(), getIndividual());
		while (raIter.hasNext()) {
			ObjectRoleAssertion ra = raIter.next().normalize(
					getIndividual().getName());
			Individual filler = aBox.getIndividual(ra.getFiller());
			Concept negConcept = qr.getConcept().copy().toggleNegated();
			ConceptSimplificationVisitor visitor = new ConceptSimplificationVisitor();
			negConcept.accept(visitor);
			negConcept = visitor.getNormalForm();
			if (!filler.contains(qr.getConcept())
					&& !filler.contains(negConcept)) {
				branchForConcepts(ra, qr.getConcept(), negConcept);
				applied = true;
				throw new BranchingException();
			}
		}
	}

	private void branchForConcepts(ObjectRoleAssertion ra, Concept lhs,
			Concept rhs) throws UnsatisfiableException {
		ConceptAssertion assert1 = new ConceptAssertion(lhs, ra.getFiller());
		ConceptAssertion assert2 = new ConceptAssertion(rhs, ra.getFiller());
		ChooseRuleBranchingPoint bp = new ChooseRuleBranchingPoint();
		bp.setWcs(getWcs());
		bp.setWorld(getWorld());
		bp.addFormula(assert1);
		bp.addFormula(assert2);
		bp.setBranchCause(reasonForApplication);
		bp.setRoleAssertion(ra);
		prover.addBranch(bp);
		getWcs().getData().getLogger().info(
				"WCS " + getWcs().getId() + " Choose rule: Branching for "
						+ assert1 + " and " + assert2);

	}
}
